
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{Instr} : \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_skip}          : \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_assign\_bool}   : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{BoolExp}   \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_assign\_nat}    : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{ArithExp}  \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_assign\_int}    : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{ArithExp}  \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_assign\_byte}   : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{ByteExp}   \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_assign\_matrix} : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{MatrixExp} \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_seq}           : \coqdocvar{Instr}   \ensuremath{\rightarrow} \coqdocvar{Instr}     \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_if}            : \coqdocvar{BoolExp} \ensuremath{\rightarrow} \coqdocvar{Instr}     \ensuremath{\rightarrow} \coqdocvar{Instr} \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_while}         : \coqdocvar{BoolExp} \ensuremath{\rightarrow} \coqdocvar{Instr}     \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_for}           : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{ArithExp}  \ensuremath{\rightarrow} \coqdocvar{Instr} \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{instr\_matrix\_set}    : \coqdocvar{Id}      \ensuremath{\rightarrow} \coqdocvar{ArithExp}  \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ByteExp} \ensuremath{\rightarrow} \coqdocvar{Instr}\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}
